Model checking is a fundamental tool used in the creation and verification of asynchronous and distributed systems. For example, model checkers may be used to verify distributed software systems used in a variety of technologies, fields and industries. Because the actions performed by each component of such a system may be interleaved in many ways, there can be a large number of configurations of the system as a whole.
In order to aid in verifying the correctness of an asynchronous system, an abstract model may be created and used along with a model checker which is able to enumerate all reachable system configurations. During its enumeration, the model checker can ensure that the system does not exhibit any invalid behaviors or reach any invalid states. If such an error is found then a trace of the actions that led to it can be reported back to the user. This trace information can be valuable when creating and debugging a new system. Additionally, if the model checker is unable to find any invalid behaviors, then it is evidence that the system is in fact correct. In order to enumerate all possible states of an asynchronous system, many popular model checkers treat the configuration space as an implicitly defined graph where nodes correspond to system states and edges are the possible transitions of each component. A path through this graph gives one possible interleaving of the actions that the system may perform. Once the graph is defined, an exhaustive search algorithm can then explore all reachable states of the system looking for ones that violate certain properties. As is typical with implicit graphs, however, there can be a very large number of nodes causing the search to take a prohibitive amount of time or memory.
Further, in non-model checking environments, the heuristic search and automated planning communities have been quite successful in developing new search frameworks that take advantage of modern multi-core processors to improve the performance of their algorithms. In addition, these frameworks have also been shown to be successful at offloading a significant portion of the memory requirement of a large graph search from RAM to external storage such as a hard disk.